\begin{frame}
\frametitle{Abbiegelicht Beispiel}

\begin{columns}
        \column{.50\textwidth}
				\textbf{Abbiegelicht:}\\                
               	Das Abbiegelicht leuchtet die Zone Links bzw. Rechts neben dem Fahrzeug aus. Wenn der Blinker nach links/rechts aktiviert ist wird das Abbiegelicht links/rechts aktiviert.
        \column{.45\textwidth}
				\begin{center}
				\includegraphics[height=.6\textheight]{images/ergonomics_adaptive_light.jpg} 
            	\end{center}				        		
        	
\end{columns}

\end{frame}

\begin{frame}
\frametitle{Abbiegelicht Statechart}
\begin{center}
\includegraphics[width=\textwidth]{images/Abbiegelicht.png} 
\end{center}
Im folgenden benutzen wir die Abkürzungen:
\matharray{lll}{
a.l \triangleq \text{abbiegelicht.links} & a.r \triangleq \text{abbiegelicht.rechts} & a.a \triangleq \text{abbiegelicht.aus} \\
b.l \triangleq \text{blinker.links} & b.r \triangleq \text{blinker.rechts} & b.a \triangleq \text{blinker.aus} 
}
\end{frame}

\begin{frame}
\frametitle{Aufgabenfolie Spezifikation}
\begin{exampleblock}{Aufgabe: Finde eine passende CTL Formel!}
\begin{enumerate}
%\onslide<1->{
%\item Wenn der Blinker nach links gesetzt ist dann ist das Abbiegelicht nach links aktiv.
%}
\only<1->{
\item Wenn der Blinker nach links gesetzt ist dann ist das Abbiegelicht im Zustand danach links aktiv.
}
\only<3->{
$$ \varphi \triangleq \mathsf{AG}  \; (b.l \Rightarrow \mathsf{AX} \; a.l) $$
}
\vspace*{-1.5em}
\onslide<4->{
\item Es kann nicht vorkommen das der Blinker nach rechts gesetzt ist und das Abbiegelicht nach links aktiv ist. 
}
\onslide<5->{
$$\varphi \triangleq  \neg \mathsf{ EF} \; (b.r \land a.l)$$
}
\vspace*{-1.5em}
\onslide<6->{
\item Wenn das Abbiegelicht nach links aktiv war kann es danach auch wieder nach rechts aktiv sein. 
}
\onslide<7->{
$$\varphi \triangleq  \mathsf{AG} \; (a.l \Rightarrow \mathsf{EF} \; a.r )$$
}
\vspace*{-1.5em}
\end{enumerate}
\end{exampleblock}
\end{frame}

\begin{frame}
\frametitle{Abbiegelicht Statechart (erweitert)}
Das Abbiegelicht hängt nun auch von der Geschwindigkeit ab.
\begin{center}
\includegraphics[width=.9\textwidth]{images/Abbiegelicht_Geschw.png} 
\end{center}
\begin{block}{Geschwindigkeit $v$}
$v$ nimmt Werte im Bereich $0$ bis $150$ an.
\end{block}
\end{frame}

\begin{frame}
\frametitle{CTL Tree des Abbiegelichts}
\begin{center}
\begin{tikzpicture}[scale = .8,every tree node/.style={draw,circle ,align=center,font=\tiny,minimum size=1.4cm},
   level distance=3cm,sibling distance=.3cm, 
   edge from parent path={(\tikzparentnode) -- (\tikzchildnode)}]
\Tree [.\node[red] {b.a \\ a.a \\ v=0}; 
    	[.{b.l \\ a.a \\ v=0 } ]    	
    	[.\node[minimum size=1cm,draw=none,align=center,font=\bfseries\tiny]{\dots}; ]
    	[.{b.l \\ a.a \\ v=150 } ]
    	[.{b.a\\ a.a \\ v=0} ]
	    [.\node[minimum size=1cm,draw=none,align=center,font=\bfseries\tiny]{\dots}; ]
    	[.{b.a\\ a.a \\ v=150} ]
		[.{b.r\\ a.a \\ v=0} ]
	   	[.\node[minimum size=1cm,draw=none,align=center,font=\bfseries\tiny]{\dots}; ]
		[.{b.r\\ a.a \\ v=150} ]
    ]
\end{tikzpicture}

\begin{block}{Problem: Zustandsexplosion}
Jeder Variablenwert bildet einen neuen Zustand und lässt die Zustandsmenge exponentiell wachsen.

Ziel: Die Variablen sollten nur wenige Werte annehmen können.
\end{block}
\end{center}
\end{frame}

\begin{frame}
\frametitle{Abstraktion des Modells}
\begin{block}{Abstraktion}
Sei low $:= TRUE$ wenn $v\leq 30$ ist.\\
Sei low $:= FALSE$ wenn $v > 30$ ist.
\end{block}
\begin{center}
\begin{tikzpicture}[scale = .8,every tree node/.style={draw,circle ,align=center,font=\tiny,minimum size=1.4cm},
   level distance=3cm,sibling distance=.3cm, 
   edge from parent path={(\tikzparentnode) -- (\tikzchildnode)}]
\Tree [.\node[red] {b.a \\ l.a \\ low=T}; 
    	[.{b.l \\ a.a \\ low=T} ]
    	[.{b.l \\ a.a \\ low=F} ]
    	[.{b.a\\ a.a \\ low=T} ]
    	[.{b.a\\ a.a \\ low=F} ]
		[.{b.r\\ a.a \\ low=T} ]
		[.{b.r\\ a.a \\ low=F} ]
    ]
\end{tikzpicture}
\end{center}
\end{frame}

\begin{frame}
\frametitle{Abstraktion: Eigenschaftserhaltend}
\begin{block}{Definition: Eigenschaftserhaltend}
Eigenschaftserhaltend bedeutet, dass aus der Gültigkeit einer CTL-Formel ($\texttt{Abs}\varphi$) im abstrakten Modell ($\texttt{Abs}\mathcal{M}$) immer die Gültigkeit der CTL-Formel ($\varphi$) im konkreten Modell ($\mathcal{M}$) abgeleitet werden kann: $$(\texttt{Abs}\mathcal{M} \vDash \texttt{Abs}\varphi) \Rightarrow (\mathcal{M} \vDash \varphi)$$
\end{block}
\end{frame}

\begin{frame}
\frametitle{Problem: Hierarchische Modelle}
\begin{center}
\includegraphics[width=.85\textwidth]{images/Hierarchie.png} 
\end{center}
\begin{block}{Hierarchie und flache Struktur}
Eine Hierarchie dient primär zur Übersicht.
Gängige \emph{Model-Checker} unterstützen keine hierarchischen Modelle.
Hierarchische Modelle müssen in flache Modelle überführt werden.
\end{block}
\vspace{1cm}
\end{frame}

\begin{frame}
\frametitle{Arten von \emph{Model-Checkern}}
Es gibt grob zwei Varianten von \emph{Model-Checkern}:
\begin{itemize}
\item \emph{Model-Checker} die auf Modellen arbeiten
\item \emph{Model-Checker} die auf Code arbeiten
\end{itemize}
\vspace{.7cm}
Ein prominenter \emph{Model-Checker} ist der EmbeddedValidator.
\begin{itemize}
\item[$\rightarrow$] Basiert auf Targetlink
\item[$\rightarrow$] Arbeitet auf Code, nicht auf der Modell-Ebene
\item[$\rightarrow$] Ist kommerziell
\end{itemize}
\vspace{.5cm}
Neben weiteren \emph{Model-Checkern} wie \textbf{Safety Checker Blockset} oder \textbf{CheckMate} gibt es auch den \textbf{Symbolic Model Verifier} (SMV)
\end{frame}
